$\forall$${\it the\_es}$:ES, ${\it e'}$, $e$:E.
\\[0ex]($e$ $\in$ before(${\it e'}$)) $\Rightarrow$ ($\exists$$l$:E List. (before(${\it e'}$) = (before($e$) @ [$e$] @ $l$) $\in$ (E List)))